equality (definitional, propositional, computational, judgemental, extensional, intensional, decidable)
identity type, equivalence of types, definitional isomorphism
isomorphism, weak equivalence, homotopy equivalence, weak homotopy equivalence, equivalence in an (∞,1)-category
Examples.
The identity functor on a category is the functor that maps each object and morphism of to itself. The identity functors are the identities for composition of functors in Cat.
Last revised on December 1, 2019 at 08:18:30. See the history of this page for a list of all contributions to it.